↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_agg(X1s, cons(X, X2s), Xs))
ap1_in_agg(nil, X, X) → ap1_out_agg(nil, X, X)
ap1_in_agg(cons(H, X), Y, cons(H, Z)) → U1_agg(H, X, Y, Z, ap1_in_aga(X, Y, Z))
ap1_in_aga(nil, X, X) → ap1_out_aga(nil, X, X)
ap1_in_aga(cons(H, X), Y, cons(H, Z)) → U1_aga(H, X, Y, Z, ap1_in_aga(X, Y, Z))
U1_aga(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons(H, X), Y, cons(H, Z))
U1_agg(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_agg(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
ap2_in_gaa(nil, X, X) → ap2_out_gaa(nil, X, X)
ap2_in_gaa(cons(H, X), Y, cons(H, Z)) → U2_gaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
ap2_in_aaa(nil, X, X) → ap2_out_aaa(nil, X, X)
ap2_in_aaa(cons(H, X), Y, cons(H, Z)) → U2_aaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
U2_aaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_aaa(cons(H, X), Y, cons(H, Z))
U2_gaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_gaa(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_aa(Zs, Ys))
perm_in_aa(nil, nil) → perm_out_aa(nil, nil)
perm_in_aa(Xs, cons(X, Ys)) → U3_aa(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
U3_aa(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_aa(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U4_aa(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_aa(Xs, X, Ys, perm_in_aa(Zs, Ys))
U5_aa(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_aa(Xs, cons(X, Ys))
U5_ga(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PrologToPiTRSProof
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_agg(X1s, cons(X, X2s), Xs))
ap1_in_agg(nil, X, X) → ap1_out_agg(nil, X, X)
ap1_in_agg(cons(H, X), Y, cons(H, Z)) → U1_agg(H, X, Y, Z, ap1_in_aga(X, Y, Z))
ap1_in_aga(nil, X, X) → ap1_out_aga(nil, X, X)
ap1_in_aga(cons(H, X), Y, cons(H, Z)) → U1_aga(H, X, Y, Z, ap1_in_aga(X, Y, Z))
U1_aga(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons(H, X), Y, cons(H, Z))
U1_agg(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_agg(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
ap2_in_gaa(nil, X, X) → ap2_out_gaa(nil, X, X)
ap2_in_gaa(cons(H, X), Y, cons(H, Z)) → U2_gaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
ap2_in_aaa(nil, X, X) → ap2_out_aaa(nil, X, X)
ap2_in_aaa(cons(H, X), Y, cons(H, Z)) → U2_aaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
U2_aaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_aaa(cons(H, X), Y, cons(H, Z))
U2_gaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_gaa(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_aa(Zs, Ys))
perm_in_aa(nil, nil) → perm_out_aa(nil, nil)
perm_in_aa(Xs, cons(X, Ys)) → U3_aa(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
U3_aa(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_aa(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U4_aa(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_aa(Xs, X, Ys, perm_in_aa(Zs, Ys))
U5_aa(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_aa(Xs, cons(X, Ys))
U5_ga(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
PERM_IN_GA(Xs, cons(X, Ys)) → U3_GA(Xs, X, Ys, ap1_in_agg(X1s, cons(X, X2s), Xs))
PERM_IN_GA(Xs, cons(X, Ys)) → AP1_IN_AGG(X1s, cons(X, X2s), Xs)
AP1_IN_AGG(cons(H, X), Y, cons(H, Z)) → U1_AGG(H, X, Y, Z, ap1_in_aga(X, Y, Z))
AP1_IN_AGG(cons(H, X), Y, cons(H, Z)) → AP1_IN_AGA(X, Y, Z)
AP1_IN_AGA(cons(H, X), Y, cons(H, Z)) → U1_AGA(H, X, Y, Z, ap1_in_aga(X, Y, Z))
AP1_IN_AGA(cons(H, X), Y, cons(H, Z)) → AP1_IN_AGA(X, Y, Z)
U3_GA(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → U4_GA(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U3_GA(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → AP2_IN_GAA(X1s, X2s, Zs)
AP2_IN_GAA(cons(H, X), Y, cons(H, Z)) → U2_GAA(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
AP2_IN_GAA(cons(H, X), Y, cons(H, Z)) → AP2_IN_AAA(X, Y, Z)
AP2_IN_AAA(cons(H, X), Y, cons(H, Z)) → U2_AAA(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
AP2_IN_AAA(cons(H, X), Y, cons(H, Z)) → AP2_IN_AAA(X, Y, Z)
U4_GA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_GA(Xs, X, Ys, perm_in_aa(Zs, Ys))
U4_GA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → PERM_IN_AA(Zs, Ys)
PERM_IN_AA(Xs, cons(X, Ys)) → U3_AA(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
PERM_IN_AA(Xs, cons(X, Ys)) → AP1_IN_AGA(X1s, cons(X, X2s), Xs)
U3_AA(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_AA(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U3_AA(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → AP2_IN_GAA(X1s, X2s, Zs)
U4_AA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_AA(Xs, X, Ys, perm_in_aa(Zs, Ys))
U4_AA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → PERM_IN_AA(Zs, Ys)
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_agg(X1s, cons(X, X2s), Xs))
ap1_in_agg(nil, X, X) → ap1_out_agg(nil, X, X)
ap1_in_agg(cons(H, X), Y, cons(H, Z)) → U1_agg(H, X, Y, Z, ap1_in_aga(X, Y, Z))
ap1_in_aga(nil, X, X) → ap1_out_aga(nil, X, X)
ap1_in_aga(cons(H, X), Y, cons(H, Z)) → U1_aga(H, X, Y, Z, ap1_in_aga(X, Y, Z))
U1_aga(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons(H, X), Y, cons(H, Z))
U1_agg(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_agg(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
ap2_in_gaa(nil, X, X) → ap2_out_gaa(nil, X, X)
ap2_in_gaa(cons(H, X), Y, cons(H, Z)) → U2_gaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
ap2_in_aaa(nil, X, X) → ap2_out_aaa(nil, X, X)
ap2_in_aaa(cons(H, X), Y, cons(H, Z)) → U2_aaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
U2_aaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_aaa(cons(H, X), Y, cons(H, Z))
U2_gaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_gaa(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_aa(Zs, Ys))
perm_in_aa(nil, nil) → perm_out_aa(nil, nil)
perm_in_aa(Xs, cons(X, Ys)) → U3_aa(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
U3_aa(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_aa(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U4_aa(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_aa(Xs, X, Ys, perm_in_aa(Zs, Ys))
U5_aa(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_aa(Xs, cons(X, Ys))
U5_ga(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ PrologToPiTRSProof
PERM_IN_GA(Xs, cons(X, Ys)) → U3_GA(Xs, X, Ys, ap1_in_agg(X1s, cons(X, X2s), Xs))
PERM_IN_GA(Xs, cons(X, Ys)) → AP1_IN_AGG(X1s, cons(X, X2s), Xs)
AP1_IN_AGG(cons(H, X), Y, cons(H, Z)) → U1_AGG(H, X, Y, Z, ap1_in_aga(X, Y, Z))
AP1_IN_AGG(cons(H, X), Y, cons(H, Z)) → AP1_IN_AGA(X, Y, Z)
AP1_IN_AGA(cons(H, X), Y, cons(H, Z)) → U1_AGA(H, X, Y, Z, ap1_in_aga(X, Y, Z))
AP1_IN_AGA(cons(H, X), Y, cons(H, Z)) → AP1_IN_AGA(X, Y, Z)
U3_GA(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → U4_GA(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U3_GA(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → AP2_IN_GAA(X1s, X2s, Zs)
AP2_IN_GAA(cons(H, X), Y, cons(H, Z)) → U2_GAA(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
AP2_IN_GAA(cons(H, X), Y, cons(H, Z)) → AP2_IN_AAA(X, Y, Z)
AP2_IN_AAA(cons(H, X), Y, cons(H, Z)) → U2_AAA(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
AP2_IN_AAA(cons(H, X), Y, cons(H, Z)) → AP2_IN_AAA(X, Y, Z)
U4_GA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_GA(Xs, X, Ys, perm_in_aa(Zs, Ys))
U4_GA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → PERM_IN_AA(Zs, Ys)
PERM_IN_AA(Xs, cons(X, Ys)) → U3_AA(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
PERM_IN_AA(Xs, cons(X, Ys)) → AP1_IN_AGA(X1s, cons(X, X2s), Xs)
U3_AA(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_AA(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U3_AA(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → AP2_IN_GAA(X1s, X2s, Zs)
U4_AA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_AA(Xs, X, Ys, perm_in_aa(Zs, Ys))
U4_AA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → PERM_IN_AA(Zs, Ys)
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_agg(X1s, cons(X, X2s), Xs))
ap1_in_agg(nil, X, X) → ap1_out_agg(nil, X, X)
ap1_in_agg(cons(H, X), Y, cons(H, Z)) → U1_agg(H, X, Y, Z, ap1_in_aga(X, Y, Z))
ap1_in_aga(nil, X, X) → ap1_out_aga(nil, X, X)
ap1_in_aga(cons(H, X), Y, cons(H, Z)) → U1_aga(H, X, Y, Z, ap1_in_aga(X, Y, Z))
U1_aga(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons(H, X), Y, cons(H, Z))
U1_agg(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_agg(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
ap2_in_gaa(nil, X, X) → ap2_out_gaa(nil, X, X)
ap2_in_gaa(cons(H, X), Y, cons(H, Z)) → U2_gaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
ap2_in_aaa(nil, X, X) → ap2_out_aaa(nil, X, X)
ap2_in_aaa(cons(H, X), Y, cons(H, Z)) → U2_aaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
U2_aaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_aaa(cons(H, X), Y, cons(H, Z))
U2_gaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_gaa(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_aa(Zs, Ys))
perm_in_aa(nil, nil) → perm_out_aa(nil, nil)
perm_in_aa(Xs, cons(X, Ys)) → U3_aa(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
U3_aa(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_aa(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U4_aa(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_aa(Xs, X, Ys, perm_in_aa(Zs, Ys))
U5_aa(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_aa(Xs, cons(X, Ys))
U5_ga(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
AP2_IN_AAA(cons(H, X), Y, cons(H, Z)) → AP2_IN_AAA(X, Y, Z)
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_agg(X1s, cons(X, X2s), Xs))
ap1_in_agg(nil, X, X) → ap1_out_agg(nil, X, X)
ap1_in_agg(cons(H, X), Y, cons(H, Z)) → U1_agg(H, X, Y, Z, ap1_in_aga(X, Y, Z))
ap1_in_aga(nil, X, X) → ap1_out_aga(nil, X, X)
ap1_in_aga(cons(H, X), Y, cons(H, Z)) → U1_aga(H, X, Y, Z, ap1_in_aga(X, Y, Z))
U1_aga(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons(H, X), Y, cons(H, Z))
U1_agg(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_agg(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
ap2_in_gaa(nil, X, X) → ap2_out_gaa(nil, X, X)
ap2_in_gaa(cons(H, X), Y, cons(H, Z)) → U2_gaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
ap2_in_aaa(nil, X, X) → ap2_out_aaa(nil, X, X)
ap2_in_aaa(cons(H, X), Y, cons(H, Z)) → U2_aaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
U2_aaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_aaa(cons(H, X), Y, cons(H, Z))
U2_gaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_gaa(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_aa(Zs, Ys))
perm_in_aa(nil, nil) → perm_out_aa(nil, nil)
perm_in_aa(Xs, cons(X, Ys)) → U3_aa(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
U3_aa(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_aa(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U4_aa(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_aa(Xs, X, Ys, perm_in_aa(Zs, Ys))
U5_aa(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_aa(Xs, cons(X, Ys))
U5_ga(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
AP2_IN_AAA(cons(H, X), Y, cons(H, Z)) → AP2_IN_AAA(X, Y, Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PiDP
↳ PiDP
↳ PrologToPiTRSProof
AP2_IN_AAA → AP2_IN_AAA
AP2_IN_AAA → AP2_IN_AAA
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PrologToPiTRSProof
AP1_IN_AGA(cons(H, X), Y, cons(H, Z)) → AP1_IN_AGA(X, Y, Z)
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_agg(X1s, cons(X, X2s), Xs))
ap1_in_agg(nil, X, X) → ap1_out_agg(nil, X, X)
ap1_in_agg(cons(H, X), Y, cons(H, Z)) → U1_agg(H, X, Y, Z, ap1_in_aga(X, Y, Z))
ap1_in_aga(nil, X, X) → ap1_out_aga(nil, X, X)
ap1_in_aga(cons(H, X), Y, cons(H, Z)) → U1_aga(H, X, Y, Z, ap1_in_aga(X, Y, Z))
U1_aga(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons(H, X), Y, cons(H, Z))
U1_agg(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_agg(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
ap2_in_gaa(nil, X, X) → ap2_out_gaa(nil, X, X)
ap2_in_gaa(cons(H, X), Y, cons(H, Z)) → U2_gaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
ap2_in_aaa(nil, X, X) → ap2_out_aaa(nil, X, X)
ap2_in_aaa(cons(H, X), Y, cons(H, Z)) → U2_aaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
U2_aaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_aaa(cons(H, X), Y, cons(H, Z))
U2_gaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_gaa(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_aa(Zs, Ys))
perm_in_aa(nil, nil) → perm_out_aa(nil, nil)
perm_in_aa(Xs, cons(X, Ys)) → U3_aa(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
U3_aa(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_aa(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U4_aa(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_aa(Xs, X, Ys, perm_in_aa(Zs, Ys))
U5_aa(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_aa(Xs, cons(X, Ys))
U5_ga(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PrologToPiTRSProof
AP1_IN_AGA(cons(H, X), Y, cons(H, Z)) → AP1_IN_AGA(X, Y, Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PiDP
↳ PrologToPiTRSProof
AP1_IN_AGA(Y) → AP1_IN_AGA(Y)
AP1_IN_AGA(Y) → AP1_IN_AGA(Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
U4_AA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → PERM_IN_AA(Zs, Ys)
U3_AA(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_AA(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
PERM_IN_AA(Xs, cons(X, Ys)) → U3_AA(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_agg(X1s, cons(X, X2s), Xs))
ap1_in_agg(nil, X, X) → ap1_out_agg(nil, X, X)
ap1_in_agg(cons(H, X), Y, cons(H, Z)) → U1_agg(H, X, Y, Z, ap1_in_aga(X, Y, Z))
ap1_in_aga(nil, X, X) → ap1_out_aga(nil, X, X)
ap1_in_aga(cons(H, X), Y, cons(H, Z)) → U1_aga(H, X, Y, Z, ap1_in_aga(X, Y, Z))
U1_aga(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons(H, X), Y, cons(H, Z))
U1_agg(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_agg(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
ap2_in_gaa(nil, X, X) → ap2_out_gaa(nil, X, X)
ap2_in_gaa(cons(H, X), Y, cons(H, Z)) → U2_gaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
ap2_in_aaa(nil, X, X) → ap2_out_aaa(nil, X, X)
ap2_in_aaa(cons(H, X), Y, cons(H, Z)) → U2_aaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
U2_aaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_aaa(cons(H, X), Y, cons(H, Z))
U2_gaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_gaa(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_aa(Zs, Ys))
perm_in_aa(nil, nil) → perm_out_aa(nil, nil)
perm_in_aa(Xs, cons(X, Ys)) → U3_aa(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
U3_aa(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_aa(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U4_aa(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_aa(Xs, X, Ys, perm_in_aa(Zs, Ys))
U5_aa(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_aa(Xs, cons(X, Ys))
U5_ga(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PrologToPiTRSProof
U4_AA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → PERM_IN_AA(Zs, Ys)
U3_AA(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_AA(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
PERM_IN_AA(Xs, cons(X, Ys)) → U3_AA(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
ap2_in_gaa(nil, X, X) → ap2_out_gaa(nil, X, X)
ap2_in_gaa(cons(H, X), Y, cons(H, Z)) → U2_gaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
ap1_in_aga(nil, X, X) → ap1_out_aga(nil, X, X)
ap1_in_aga(cons(H, X), Y, cons(H, Z)) → U1_aga(H, X, Y, Z, ap1_in_aga(X, Y, Z))
U2_gaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_gaa(cons(H, X), Y, cons(H, Z))
U1_aga(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons(H, X), Y, cons(H, Z))
ap2_in_aaa(nil, X, X) → ap2_out_aaa(nil, X, X)
ap2_in_aaa(cons(H, X), Y, cons(H, Z)) → U2_aaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
U2_aaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_aaa(cons(H, X), Y, cons(H, Z))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ PrologToPiTRSProof
U4_AA(Xs, ap2_out_gaa) → PERM_IN_AA
PERM_IN_AA → U3_AA(ap1_in_aga(cons))
U3_AA(ap1_out_aga(X1s, Xs)) → U4_AA(Xs, ap2_in_gaa(X1s))
ap2_in_gaa(nil) → ap2_out_gaa
ap2_in_gaa(cons) → U2_gaa(ap2_in_aaa)
ap1_in_aga(X) → ap1_out_aga(nil, X)
ap1_in_aga(Y) → U1_aga(ap1_in_aga(Y))
U2_gaa(ap2_out_aaa(X)) → ap2_out_gaa
U1_aga(ap1_out_aga(X, Z)) → ap1_out_aga(cons, cons)
ap2_in_aaa → ap2_out_aaa(nil)
ap2_in_aaa → U2_aaa(ap2_in_aaa)
U2_aaa(ap2_out_aaa(X)) → ap2_out_aaa(cons)
ap2_in_gaa(x0)
ap1_in_aga(x0)
U2_gaa(x0)
U1_aga(x0)
ap2_in_aaa
U2_aaa(x0)
U3_AA(ap1_out_aga(nil, y1)) → U4_AA(y1, ap2_out_gaa)
U3_AA(ap1_out_aga(cons, y1)) → U4_AA(y1, U2_gaa(ap2_in_aaa))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ PrologToPiTRSProof
U3_AA(ap1_out_aga(nil, y1)) → U4_AA(y1, ap2_out_gaa)
U4_AA(Xs, ap2_out_gaa) → PERM_IN_AA
U3_AA(ap1_out_aga(cons, y1)) → U4_AA(y1, U2_gaa(ap2_in_aaa))
PERM_IN_AA → U3_AA(ap1_in_aga(cons))
ap2_in_gaa(nil) → ap2_out_gaa
ap2_in_gaa(cons) → U2_gaa(ap2_in_aaa)
ap1_in_aga(X) → ap1_out_aga(nil, X)
ap1_in_aga(Y) → U1_aga(ap1_in_aga(Y))
U2_gaa(ap2_out_aaa(X)) → ap2_out_gaa
U1_aga(ap1_out_aga(X, Z)) → ap1_out_aga(cons, cons)
ap2_in_aaa → ap2_out_aaa(nil)
ap2_in_aaa → U2_aaa(ap2_in_aaa)
U2_aaa(ap2_out_aaa(X)) → ap2_out_aaa(cons)
ap2_in_gaa(x0)
ap1_in_aga(x0)
U2_gaa(x0)
U1_aga(x0)
ap2_in_aaa
U2_aaa(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ PrologToPiTRSProof
U3_AA(ap1_out_aga(nil, y1)) → U4_AA(y1, ap2_out_gaa)
U4_AA(Xs, ap2_out_gaa) → PERM_IN_AA
U3_AA(ap1_out_aga(cons, y1)) → U4_AA(y1, U2_gaa(ap2_in_aaa))
PERM_IN_AA → U3_AA(ap1_in_aga(cons))
ap1_in_aga(X) → ap1_out_aga(nil, X)
ap1_in_aga(Y) → U1_aga(ap1_in_aga(Y))
U1_aga(ap1_out_aga(X, Z)) → ap1_out_aga(cons, cons)
ap2_in_aaa → ap2_out_aaa(nil)
ap2_in_aaa → U2_aaa(ap2_in_aaa)
U2_gaa(ap2_out_aaa(X)) → ap2_out_gaa
U2_aaa(ap2_out_aaa(X)) → ap2_out_aaa(cons)
ap2_in_gaa(x0)
ap1_in_aga(x0)
U2_gaa(x0)
U1_aga(x0)
ap2_in_aaa
U2_aaa(x0)
ap2_in_gaa(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ PrologToPiTRSProof
U4_AA(Xs, ap2_out_gaa) → PERM_IN_AA
U3_AA(ap1_out_aga(nil, y1)) → U4_AA(y1, ap2_out_gaa)
PERM_IN_AA → U3_AA(ap1_in_aga(cons))
U3_AA(ap1_out_aga(cons, y1)) → U4_AA(y1, U2_gaa(ap2_in_aaa))
ap1_in_aga(X) → ap1_out_aga(nil, X)
ap1_in_aga(Y) → U1_aga(ap1_in_aga(Y))
U1_aga(ap1_out_aga(X, Z)) → ap1_out_aga(cons, cons)
ap2_in_aaa → ap2_out_aaa(nil)
ap2_in_aaa → U2_aaa(ap2_in_aaa)
U2_gaa(ap2_out_aaa(X)) → ap2_out_gaa
U2_aaa(ap2_out_aaa(X)) → ap2_out_aaa(cons)
ap1_in_aga(x0)
U2_gaa(x0)
U1_aga(x0)
ap2_in_aaa
U2_aaa(x0)
PERM_IN_AA → U3_AA(ap1_out_aga(nil, cons))
PERM_IN_AA → U3_AA(U1_aga(ap1_in_aga(cons)))
↳ Prolog
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ NonTerminationProof
↳ PrologToPiTRSProof
PERM_IN_AA → U3_AA(U1_aga(ap1_in_aga(cons)))
U3_AA(ap1_out_aga(nil, y1)) → U4_AA(y1, ap2_out_gaa)
U4_AA(Xs, ap2_out_gaa) → PERM_IN_AA
PERM_IN_AA → U3_AA(ap1_out_aga(nil, cons))
U3_AA(ap1_out_aga(cons, y1)) → U4_AA(y1, U2_gaa(ap2_in_aaa))
ap1_in_aga(X) → ap1_out_aga(nil, X)
ap1_in_aga(Y) → U1_aga(ap1_in_aga(Y))
U1_aga(ap1_out_aga(X, Z)) → ap1_out_aga(cons, cons)
ap2_in_aaa → ap2_out_aaa(nil)
ap2_in_aaa → U2_aaa(ap2_in_aaa)
U2_gaa(ap2_out_aaa(X)) → ap2_out_gaa
U2_aaa(ap2_out_aaa(X)) → ap2_out_aaa(cons)
ap1_in_aga(x0)
U2_gaa(x0)
U1_aga(x0)
ap2_in_aaa
U2_aaa(x0)
PERM_IN_AA → U3_AA(U1_aga(ap1_in_aga(cons)))
U3_AA(ap1_out_aga(nil, y1)) → U4_AA(y1, ap2_out_gaa)
U4_AA(Xs, ap2_out_gaa) → PERM_IN_AA
PERM_IN_AA → U3_AA(ap1_out_aga(nil, cons))
U3_AA(ap1_out_aga(cons, y1)) → U4_AA(y1, U2_gaa(ap2_in_aaa))
ap1_in_aga(X) → ap1_out_aga(nil, X)
ap1_in_aga(Y) → U1_aga(ap1_in_aga(Y))
U1_aga(ap1_out_aga(X, Z)) → ap1_out_aga(cons, cons)
ap2_in_aaa → ap2_out_aaa(nil)
ap2_in_aaa → U2_aaa(ap2_in_aaa)
U2_gaa(ap2_out_aaa(X)) → ap2_out_gaa
U2_aaa(ap2_out_aaa(X)) → ap2_out_aaa(cons)
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_agg(X1s, cons(X, X2s), Xs))
ap1_in_agg(nil, X, X) → ap1_out_agg(nil, X, X)
ap1_in_agg(cons(H, X), Y, cons(H, Z)) → U1_agg(H, X, Y, Z, ap1_in_aga(X, Y, Z))
ap1_in_aga(nil, X, X) → ap1_out_aga(nil, X, X)
ap1_in_aga(cons(H, X), Y, cons(H, Z)) → U1_aga(H, X, Y, Z, ap1_in_aga(X, Y, Z))
U1_aga(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons(H, X), Y, cons(H, Z))
U1_agg(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_agg(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
ap2_in_gaa(nil, X, X) → ap2_out_gaa(nil, X, X)
ap2_in_gaa(cons(H, X), Y, cons(H, Z)) → U2_gaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
ap2_in_aaa(nil, X, X) → ap2_out_aaa(nil, X, X)
ap2_in_aaa(cons(H, X), Y, cons(H, Z)) → U2_aaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
U2_aaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_aaa(cons(H, X), Y, cons(H, Z))
U2_gaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_gaa(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_aa(Zs, Ys))
perm_in_aa(nil, nil) → perm_out_aa(nil, nil)
perm_in_aa(Xs, cons(X, Ys)) → U3_aa(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
U3_aa(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_aa(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U4_aa(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_aa(Xs, X, Ys, perm_in_aa(Zs, Ys))
U5_aa(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_aa(Xs, cons(X, Ys))
U5_ga(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_agg(X1s, cons(X, X2s), Xs))
ap1_in_agg(nil, X, X) → ap1_out_agg(nil, X, X)
ap1_in_agg(cons(H, X), Y, cons(H, Z)) → U1_agg(H, X, Y, Z, ap1_in_aga(X, Y, Z))
ap1_in_aga(nil, X, X) → ap1_out_aga(nil, X, X)
ap1_in_aga(cons(H, X), Y, cons(H, Z)) → U1_aga(H, X, Y, Z, ap1_in_aga(X, Y, Z))
U1_aga(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons(H, X), Y, cons(H, Z))
U1_agg(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_agg(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
ap2_in_gaa(nil, X, X) → ap2_out_gaa(nil, X, X)
ap2_in_gaa(cons(H, X), Y, cons(H, Z)) → U2_gaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
ap2_in_aaa(nil, X, X) → ap2_out_aaa(nil, X, X)
ap2_in_aaa(cons(H, X), Y, cons(H, Z)) → U2_aaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
U2_aaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_aaa(cons(H, X), Y, cons(H, Z))
U2_gaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_gaa(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_aa(Zs, Ys))
perm_in_aa(nil, nil) → perm_out_aa(nil, nil)
perm_in_aa(Xs, cons(X, Ys)) → U3_aa(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
U3_aa(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_aa(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U4_aa(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_aa(Xs, X, Ys, perm_in_aa(Zs, Ys))
U5_aa(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_aa(Xs, cons(X, Ys))
U5_ga(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
PERM_IN_GA(Xs, cons(X, Ys)) → U3_GA(Xs, X, Ys, ap1_in_agg(X1s, cons(X, X2s), Xs))
PERM_IN_GA(Xs, cons(X, Ys)) → AP1_IN_AGG(X1s, cons(X, X2s), Xs)
AP1_IN_AGG(cons(H, X), Y, cons(H, Z)) → U1_AGG(H, X, Y, Z, ap1_in_aga(X, Y, Z))
AP1_IN_AGG(cons(H, X), Y, cons(H, Z)) → AP1_IN_AGA(X, Y, Z)
AP1_IN_AGA(cons(H, X), Y, cons(H, Z)) → U1_AGA(H, X, Y, Z, ap1_in_aga(X, Y, Z))
AP1_IN_AGA(cons(H, X), Y, cons(H, Z)) → AP1_IN_AGA(X, Y, Z)
U3_GA(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → U4_GA(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U3_GA(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → AP2_IN_GAA(X1s, X2s, Zs)
AP2_IN_GAA(cons(H, X), Y, cons(H, Z)) → U2_GAA(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
AP2_IN_GAA(cons(H, X), Y, cons(H, Z)) → AP2_IN_AAA(X, Y, Z)
AP2_IN_AAA(cons(H, X), Y, cons(H, Z)) → U2_AAA(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
AP2_IN_AAA(cons(H, X), Y, cons(H, Z)) → AP2_IN_AAA(X, Y, Z)
U4_GA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_GA(Xs, X, Ys, perm_in_aa(Zs, Ys))
U4_GA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → PERM_IN_AA(Zs, Ys)
PERM_IN_AA(Xs, cons(X, Ys)) → U3_AA(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
PERM_IN_AA(Xs, cons(X, Ys)) → AP1_IN_AGA(X1s, cons(X, X2s), Xs)
U3_AA(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_AA(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U3_AA(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → AP2_IN_GAA(X1s, X2s, Zs)
U4_AA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_AA(Xs, X, Ys, perm_in_aa(Zs, Ys))
U4_AA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → PERM_IN_AA(Zs, Ys)
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_agg(X1s, cons(X, X2s), Xs))
ap1_in_agg(nil, X, X) → ap1_out_agg(nil, X, X)
ap1_in_agg(cons(H, X), Y, cons(H, Z)) → U1_agg(H, X, Y, Z, ap1_in_aga(X, Y, Z))
ap1_in_aga(nil, X, X) → ap1_out_aga(nil, X, X)
ap1_in_aga(cons(H, X), Y, cons(H, Z)) → U1_aga(H, X, Y, Z, ap1_in_aga(X, Y, Z))
U1_aga(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons(H, X), Y, cons(H, Z))
U1_agg(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_agg(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
ap2_in_gaa(nil, X, X) → ap2_out_gaa(nil, X, X)
ap2_in_gaa(cons(H, X), Y, cons(H, Z)) → U2_gaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
ap2_in_aaa(nil, X, X) → ap2_out_aaa(nil, X, X)
ap2_in_aaa(cons(H, X), Y, cons(H, Z)) → U2_aaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
U2_aaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_aaa(cons(H, X), Y, cons(H, Z))
U2_gaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_gaa(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_aa(Zs, Ys))
perm_in_aa(nil, nil) → perm_out_aa(nil, nil)
perm_in_aa(Xs, cons(X, Ys)) → U3_aa(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
U3_aa(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_aa(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U4_aa(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_aa(Xs, X, Ys, perm_in_aa(Zs, Ys))
U5_aa(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_aa(Xs, cons(X, Ys))
U5_ga(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
PERM_IN_GA(Xs, cons(X, Ys)) → U3_GA(Xs, X, Ys, ap1_in_agg(X1s, cons(X, X2s), Xs))
PERM_IN_GA(Xs, cons(X, Ys)) → AP1_IN_AGG(X1s, cons(X, X2s), Xs)
AP1_IN_AGG(cons(H, X), Y, cons(H, Z)) → U1_AGG(H, X, Y, Z, ap1_in_aga(X, Y, Z))
AP1_IN_AGG(cons(H, X), Y, cons(H, Z)) → AP1_IN_AGA(X, Y, Z)
AP1_IN_AGA(cons(H, X), Y, cons(H, Z)) → U1_AGA(H, X, Y, Z, ap1_in_aga(X, Y, Z))
AP1_IN_AGA(cons(H, X), Y, cons(H, Z)) → AP1_IN_AGA(X, Y, Z)
U3_GA(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → U4_GA(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U3_GA(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → AP2_IN_GAA(X1s, X2s, Zs)
AP2_IN_GAA(cons(H, X), Y, cons(H, Z)) → U2_GAA(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
AP2_IN_GAA(cons(H, X), Y, cons(H, Z)) → AP2_IN_AAA(X, Y, Z)
AP2_IN_AAA(cons(H, X), Y, cons(H, Z)) → U2_AAA(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
AP2_IN_AAA(cons(H, X), Y, cons(H, Z)) → AP2_IN_AAA(X, Y, Z)
U4_GA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_GA(Xs, X, Ys, perm_in_aa(Zs, Ys))
U4_GA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → PERM_IN_AA(Zs, Ys)
PERM_IN_AA(Xs, cons(X, Ys)) → U3_AA(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
PERM_IN_AA(Xs, cons(X, Ys)) → AP1_IN_AGA(X1s, cons(X, X2s), Xs)
U3_AA(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_AA(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U3_AA(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → AP2_IN_GAA(X1s, X2s, Zs)
U4_AA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_AA(Xs, X, Ys, perm_in_aa(Zs, Ys))
U4_AA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → PERM_IN_AA(Zs, Ys)
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_agg(X1s, cons(X, X2s), Xs))
ap1_in_agg(nil, X, X) → ap1_out_agg(nil, X, X)
ap1_in_agg(cons(H, X), Y, cons(H, Z)) → U1_agg(H, X, Y, Z, ap1_in_aga(X, Y, Z))
ap1_in_aga(nil, X, X) → ap1_out_aga(nil, X, X)
ap1_in_aga(cons(H, X), Y, cons(H, Z)) → U1_aga(H, X, Y, Z, ap1_in_aga(X, Y, Z))
U1_aga(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons(H, X), Y, cons(H, Z))
U1_agg(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_agg(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
ap2_in_gaa(nil, X, X) → ap2_out_gaa(nil, X, X)
ap2_in_gaa(cons(H, X), Y, cons(H, Z)) → U2_gaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
ap2_in_aaa(nil, X, X) → ap2_out_aaa(nil, X, X)
ap2_in_aaa(cons(H, X), Y, cons(H, Z)) → U2_aaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
U2_aaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_aaa(cons(H, X), Y, cons(H, Z))
U2_gaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_gaa(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_aa(Zs, Ys))
perm_in_aa(nil, nil) → perm_out_aa(nil, nil)
perm_in_aa(Xs, cons(X, Ys)) → U3_aa(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
U3_aa(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_aa(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U4_aa(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_aa(Xs, X, Ys, perm_in_aa(Zs, Ys))
U5_aa(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_aa(Xs, cons(X, Ys))
U5_ga(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDP
AP2_IN_AAA(cons(H, X), Y, cons(H, Z)) → AP2_IN_AAA(X, Y, Z)
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_agg(X1s, cons(X, X2s), Xs))
ap1_in_agg(nil, X, X) → ap1_out_agg(nil, X, X)
ap1_in_agg(cons(H, X), Y, cons(H, Z)) → U1_agg(H, X, Y, Z, ap1_in_aga(X, Y, Z))
ap1_in_aga(nil, X, X) → ap1_out_aga(nil, X, X)
ap1_in_aga(cons(H, X), Y, cons(H, Z)) → U1_aga(H, X, Y, Z, ap1_in_aga(X, Y, Z))
U1_aga(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons(H, X), Y, cons(H, Z))
U1_agg(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_agg(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
ap2_in_gaa(nil, X, X) → ap2_out_gaa(nil, X, X)
ap2_in_gaa(cons(H, X), Y, cons(H, Z)) → U2_gaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
ap2_in_aaa(nil, X, X) → ap2_out_aaa(nil, X, X)
ap2_in_aaa(cons(H, X), Y, cons(H, Z)) → U2_aaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
U2_aaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_aaa(cons(H, X), Y, cons(H, Z))
U2_gaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_gaa(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_aa(Zs, Ys))
perm_in_aa(nil, nil) → perm_out_aa(nil, nil)
perm_in_aa(Xs, cons(X, Ys)) → U3_aa(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
U3_aa(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_aa(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U4_aa(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_aa(Xs, X, Ys, perm_in_aa(Zs, Ys))
U5_aa(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_aa(Xs, cons(X, Ys))
U5_ga(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
↳ PiDP
AP2_IN_AAA(cons(H, X), Y, cons(H, Z)) → AP2_IN_AAA(X, Y, Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PiDP
↳ PiDP
AP2_IN_AAA → AP2_IN_AAA
AP2_IN_AAA → AP2_IN_AAA
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
AP1_IN_AGA(cons(H, X), Y, cons(H, Z)) → AP1_IN_AGA(X, Y, Z)
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_agg(X1s, cons(X, X2s), Xs))
ap1_in_agg(nil, X, X) → ap1_out_agg(nil, X, X)
ap1_in_agg(cons(H, X), Y, cons(H, Z)) → U1_agg(H, X, Y, Z, ap1_in_aga(X, Y, Z))
ap1_in_aga(nil, X, X) → ap1_out_aga(nil, X, X)
ap1_in_aga(cons(H, X), Y, cons(H, Z)) → U1_aga(H, X, Y, Z, ap1_in_aga(X, Y, Z))
U1_aga(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons(H, X), Y, cons(H, Z))
U1_agg(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_agg(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
ap2_in_gaa(nil, X, X) → ap2_out_gaa(nil, X, X)
ap2_in_gaa(cons(H, X), Y, cons(H, Z)) → U2_gaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
ap2_in_aaa(nil, X, X) → ap2_out_aaa(nil, X, X)
ap2_in_aaa(cons(H, X), Y, cons(H, Z)) → U2_aaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
U2_aaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_aaa(cons(H, X), Y, cons(H, Z))
U2_gaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_gaa(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_aa(Zs, Ys))
perm_in_aa(nil, nil) → perm_out_aa(nil, nil)
perm_in_aa(Xs, cons(X, Ys)) → U3_aa(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
U3_aa(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_aa(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U4_aa(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_aa(Xs, X, Ys, perm_in_aa(Zs, Ys))
U5_aa(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_aa(Xs, cons(X, Ys))
U5_ga(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ PiDP
AP1_IN_AGA(cons(H, X), Y, cons(H, Z)) → AP1_IN_AGA(X, Y, Z)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ NonTerminationProof
↳ PiDP
AP1_IN_AGA(Y) → AP1_IN_AGA(Y)
AP1_IN_AGA(Y) → AP1_IN_AGA(Y)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
U4_AA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → PERM_IN_AA(Zs, Ys)
U3_AA(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_AA(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
PERM_IN_AA(Xs, cons(X, Ys)) → U3_AA(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
perm_in_ga(nil, nil) → perm_out_ga(nil, nil)
perm_in_ga(Xs, cons(X, Ys)) → U3_ga(Xs, X, Ys, ap1_in_agg(X1s, cons(X, X2s), Xs))
ap1_in_agg(nil, X, X) → ap1_out_agg(nil, X, X)
ap1_in_agg(cons(H, X), Y, cons(H, Z)) → U1_agg(H, X, Y, Z, ap1_in_aga(X, Y, Z))
ap1_in_aga(nil, X, X) → ap1_out_aga(nil, X, X)
ap1_in_aga(cons(H, X), Y, cons(H, Z)) → U1_aga(H, X, Y, Z, ap1_in_aga(X, Y, Z))
U1_aga(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons(H, X), Y, cons(H, Z))
U1_agg(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_agg(cons(H, X), Y, cons(H, Z))
U3_ga(Xs, X, Ys, ap1_out_agg(X1s, cons(X, X2s), Xs)) → U4_ga(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
ap2_in_gaa(nil, X, X) → ap2_out_gaa(nil, X, X)
ap2_in_gaa(cons(H, X), Y, cons(H, Z)) → U2_gaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
ap2_in_aaa(nil, X, X) → ap2_out_aaa(nil, X, X)
ap2_in_aaa(cons(H, X), Y, cons(H, Z)) → U2_aaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
U2_aaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_aaa(cons(H, X), Y, cons(H, Z))
U2_gaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_gaa(cons(H, X), Y, cons(H, Z))
U4_ga(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_ga(Xs, X, Ys, perm_in_aa(Zs, Ys))
perm_in_aa(nil, nil) → perm_out_aa(nil, nil)
perm_in_aa(Xs, cons(X, Ys)) → U3_aa(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
U3_aa(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_aa(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
U4_aa(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → U5_aa(Xs, X, Ys, perm_in_aa(Zs, Ys))
U5_aa(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_aa(Xs, cons(X, Ys))
U5_ga(Xs, X, Ys, perm_out_aa(Zs, Ys)) → perm_out_ga(Xs, cons(X, Ys))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
U4_AA(Xs, X, Ys, X1s, X2s, ap2_out_gaa(X1s, X2s, Zs)) → PERM_IN_AA(Zs, Ys)
U3_AA(Xs, X, Ys, ap1_out_aga(X1s, cons(X, X2s), Xs)) → U4_AA(Xs, X, Ys, X1s, X2s, ap2_in_gaa(X1s, X2s, Zs))
PERM_IN_AA(Xs, cons(X, Ys)) → U3_AA(Xs, X, Ys, ap1_in_aga(X1s, cons(X, X2s), Xs))
ap2_in_gaa(nil, X, X) → ap2_out_gaa(nil, X, X)
ap2_in_gaa(cons(H, X), Y, cons(H, Z)) → U2_gaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
ap1_in_aga(nil, X, X) → ap1_out_aga(nil, X, X)
ap1_in_aga(cons(H, X), Y, cons(H, Z)) → U1_aga(H, X, Y, Z, ap1_in_aga(X, Y, Z))
U2_gaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_gaa(cons(H, X), Y, cons(H, Z))
U1_aga(H, X, Y, Z, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons(H, X), Y, cons(H, Z))
ap2_in_aaa(nil, X, X) → ap2_out_aaa(nil, X, X)
ap2_in_aaa(cons(H, X), Y, cons(H, Z)) → U2_aaa(H, X, Y, Z, ap2_in_aaa(X, Y, Z))
U2_aaa(H, X, Y, Z, ap2_out_aaa(X, Y, Z)) → ap2_out_aaa(cons(H, X), Y, cons(H, Z))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
U3_AA(ap1_out_aga(X1s, cons, Xs)) → U4_AA(Xs, ap2_in_gaa(X1s))
U4_AA(Xs, ap2_out_gaa(X1s)) → PERM_IN_AA
PERM_IN_AA → U3_AA(ap1_in_aga(cons))
ap2_in_gaa(nil) → ap2_out_gaa(nil)
ap2_in_gaa(cons) → U2_gaa(ap2_in_aaa)
ap1_in_aga(X) → ap1_out_aga(nil, X, X)
ap1_in_aga(Y) → U1_aga(Y, ap1_in_aga(Y))
U2_gaa(ap2_out_aaa(X)) → ap2_out_gaa(cons)
U1_aga(Y, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons, Y, cons)
ap2_in_aaa → ap2_out_aaa(nil)
ap2_in_aaa → U2_aaa(ap2_in_aaa)
U2_aaa(ap2_out_aaa(X)) → ap2_out_aaa(cons)
ap2_in_gaa(x0)
ap1_in_aga(x0)
U2_gaa(x0)
U1_aga(x0, x1)
ap2_in_aaa
U2_aaa(x0)
U3_AA(ap1_out_aga(nil, cons, y1)) → U4_AA(y1, ap2_out_gaa(nil))
U3_AA(ap1_out_aga(cons, cons, y1)) → U4_AA(y1, U2_gaa(ap2_in_aaa))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
U3_AA(ap1_out_aga(nil, cons, y1)) → U4_AA(y1, ap2_out_gaa(nil))
U4_AA(Xs, ap2_out_gaa(X1s)) → PERM_IN_AA
U3_AA(ap1_out_aga(cons, cons, y1)) → U4_AA(y1, U2_gaa(ap2_in_aaa))
PERM_IN_AA → U3_AA(ap1_in_aga(cons))
ap2_in_gaa(nil) → ap2_out_gaa(nil)
ap2_in_gaa(cons) → U2_gaa(ap2_in_aaa)
ap1_in_aga(X) → ap1_out_aga(nil, X, X)
ap1_in_aga(Y) → U1_aga(Y, ap1_in_aga(Y))
U2_gaa(ap2_out_aaa(X)) → ap2_out_gaa(cons)
U1_aga(Y, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons, Y, cons)
ap2_in_aaa → ap2_out_aaa(nil)
ap2_in_aaa → U2_aaa(ap2_in_aaa)
U2_aaa(ap2_out_aaa(X)) → ap2_out_aaa(cons)
ap2_in_gaa(x0)
ap1_in_aga(x0)
U2_gaa(x0)
U1_aga(x0, x1)
ap2_in_aaa
U2_aaa(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
U3_AA(ap1_out_aga(nil, cons, y1)) → U4_AA(y1, ap2_out_gaa(nil))
U4_AA(Xs, ap2_out_gaa(X1s)) → PERM_IN_AA
U3_AA(ap1_out_aga(cons, cons, y1)) → U4_AA(y1, U2_gaa(ap2_in_aaa))
PERM_IN_AA → U3_AA(ap1_in_aga(cons))
ap1_in_aga(X) → ap1_out_aga(nil, X, X)
ap1_in_aga(Y) → U1_aga(Y, ap1_in_aga(Y))
U1_aga(Y, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons, Y, cons)
ap2_in_aaa → ap2_out_aaa(nil)
ap2_in_aaa → U2_aaa(ap2_in_aaa)
U2_gaa(ap2_out_aaa(X)) → ap2_out_gaa(cons)
U2_aaa(ap2_out_aaa(X)) → ap2_out_aaa(cons)
ap2_in_gaa(x0)
ap1_in_aga(x0)
U2_gaa(x0)
U1_aga(x0, x1)
ap2_in_aaa
U2_aaa(x0)
ap2_in_gaa(x0)
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
U3_AA(ap1_out_aga(nil, cons, y1)) → U4_AA(y1, ap2_out_gaa(nil))
U4_AA(Xs, ap2_out_gaa(X1s)) → PERM_IN_AA
U3_AA(ap1_out_aga(cons, cons, y1)) → U4_AA(y1, U2_gaa(ap2_in_aaa))
PERM_IN_AA → U3_AA(ap1_in_aga(cons))
ap1_in_aga(X) → ap1_out_aga(nil, X, X)
ap1_in_aga(Y) → U1_aga(Y, ap1_in_aga(Y))
U1_aga(Y, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons, Y, cons)
ap2_in_aaa → ap2_out_aaa(nil)
ap2_in_aaa → U2_aaa(ap2_in_aaa)
U2_gaa(ap2_out_aaa(X)) → ap2_out_gaa(cons)
U2_aaa(ap2_out_aaa(X)) → ap2_out_aaa(cons)
ap1_in_aga(x0)
U2_gaa(x0)
U1_aga(x0, x1)
ap2_in_aaa
U2_aaa(x0)
PERM_IN_AA → U3_AA(ap1_out_aga(nil, cons, cons))
PERM_IN_AA → U3_AA(U1_aga(cons, ap1_in_aga(cons)))
↳ Prolog
↳ PrologToPiTRSProof
↳ PrologToPiTRSProof
↳ PiTRS
↳ DependencyPairsProof
↳ PiDP
↳ DependencyGraphProof
↳ AND
↳ PiDP
↳ PiDP
↳ PiDP
↳ UsableRulesProof
↳ PiDP
↳ PiDPToQDPProof
↳ QDP
↳ Narrowing
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ NonTerminationProof
U3_AA(ap1_out_aga(nil, cons, y1)) → U4_AA(y1, ap2_out_gaa(nil))
U4_AA(Xs, ap2_out_gaa(X1s)) → PERM_IN_AA
PERM_IN_AA → U3_AA(ap1_out_aga(nil, cons, cons))
U3_AA(ap1_out_aga(cons, cons, y1)) → U4_AA(y1, U2_gaa(ap2_in_aaa))
PERM_IN_AA → U3_AA(U1_aga(cons, ap1_in_aga(cons)))
ap1_in_aga(X) → ap1_out_aga(nil, X, X)
ap1_in_aga(Y) → U1_aga(Y, ap1_in_aga(Y))
U1_aga(Y, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons, Y, cons)
ap2_in_aaa → ap2_out_aaa(nil)
ap2_in_aaa → U2_aaa(ap2_in_aaa)
U2_gaa(ap2_out_aaa(X)) → ap2_out_gaa(cons)
U2_aaa(ap2_out_aaa(X)) → ap2_out_aaa(cons)
ap1_in_aga(x0)
U2_gaa(x0)
U1_aga(x0, x1)
ap2_in_aaa
U2_aaa(x0)
U3_AA(ap1_out_aga(nil, cons, y1)) → U4_AA(y1, ap2_out_gaa(nil))
U4_AA(Xs, ap2_out_gaa(X1s)) → PERM_IN_AA
PERM_IN_AA → U3_AA(ap1_out_aga(nil, cons, cons))
U3_AA(ap1_out_aga(cons, cons, y1)) → U4_AA(y1, U2_gaa(ap2_in_aaa))
PERM_IN_AA → U3_AA(U1_aga(cons, ap1_in_aga(cons)))
ap1_in_aga(X) → ap1_out_aga(nil, X, X)
ap1_in_aga(Y) → U1_aga(Y, ap1_in_aga(Y))
U1_aga(Y, ap1_out_aga(X, Y, Z)) → ap1_out_aga(cons, Y, cons)
ap2_in_aaa → ap2_out_aaa(nil)
ap2_in_aaa → U2_aaa(ap2_in_aaa)
U2_gaa(ap2_out_aaa(X)) → ap2_out_gaa(cons)
U2_aaa(ap2_out_aaa(X)) → ap2_out_aaa(cons)